Pure Logic of Necessitation + L

動機

当たり前だが，Pure Logic of Necessitationの拡張として，証明可能性論理としては次の論理を考えたい．

T. Kurahashi, Y. Sato; "The finite frame property of some extensions of the pure logic of necessitation"のFuture Worksとして挙げられている

In the context of provability logic, one may wonder the completeness of $ \mathsf{N + GL}（$ \sf GL \equiv \Box(\Box\varphi \to \varphi) \to \Box\varphi）, which is not of the form $ \mathrm{Acc}_{m,n} and thus not covered by this paper. Many of the $ \sf N counterpart of the famous extensions of $ \sf K are still left uninvestigated.

Def

$ \sf NLは次の公理と推論規則を持つ．

Axiom

$ \sf Taut: 命題論理のトートロジー全て

$ \sf L: 様相論理の公理L: $ \Box(\Box\varphi \to \varphi) \to \Box\varphi

形式化されたLöbの定理に対応．

Rule

モーダス・ポネンス: $ \sf NL \vdash \varphiと$ \sf NL \vdash \varphi \to \psiから$ \sf NL \vdash \psiを導出

ネセシテーション: $ \sf NL \vdash \varphiから$ \sf NL \vdash \Box\varphiを導出

証明可能性述語について$ T \vdash \varphi$ \implies$ T \vdash \mathrm{Pr}_T (\overline{\ulcorner \varphi \urcorner})に対応

導出可能性条件D1．$ Tは$ \sf PAのRE拡大